package cfsmon.logic.dfm;

import java.util.Collection;
import java.util.Iterator;

import cfsmon.common.Event;
import cfsmon.common.Parameter;

public class DfmToCHeaderTranslator {

	/**
	 * This string is the introduction to the generated monitor header
	 */
	private static final String intro = "// This file was generated automatically by CFSMon";
	
	/**
	 * This message is printed out with the assertion on reaching an error state
	 */
	private static final String errorMessage = "The monitor reached an error state.";
	
	/**
	 * The header name will serve as a preprocessor variable to shield the header
	 */
	private static final String headerName = "_CFSMON_MONITOR_H";
	
	/**
	 * This prefix will stand in front of every event name to prevent an accidental
	 * mixup with monitor variables or monitor functions
	 */
	private static final String eventPrefix = "CFSMON_";
	
	/**
	 * This will be the name of the parameterless transition function
	 */
	private static final String moveFctName = "_CFSMON_move";
	
	/**
	 * This will be the name of the function that indicates a property violation
	 */
	private static final String violateFctName = "_CFSMON_violate";
	
	/**
	 * The label that optionally defines an error location
	 */
	private static final String violateLabel = "ERROR";
	
	/**
	 * Name of the function that indicates insufficient monitor space
	 */
	private static final String slotsFullFctName = "_CFSMON_slotsFull";
	
	/**
	 * The label that optionally defines an error location
	 */
	private static final String slotsFullLabel = "ERROR";
	
	/**
	 * This string will prefix every monitor state variable and parameter
	 */
	private static final String monitorVarPrefix = "_m";
	
	/**
	 * The line break
	 */
	private static final String crlf = "\r\n";
	
	/**
	 * Source code indentation unit
	 */
	private static final String indentStr = "\t";
	
	
	public static String translate(IDfm dfm){
		if (dfm != null){			
			StringBuffer header = new StringBuffer();
			
			writeOpenHeader(header);
			
			writeIncludes(header);
			
			writeSignatures(header, dfm);
			
			writeMonitorState(header, dfm);
			
			writeErrorFunctionDefinitions(header);
			
			writeMoveDefinition(header, dfm);
			
			writeEventDefinitions(header, dfm);
			
			writeCloseHeader(header);
			
			return header.toString();
		} else {
			return null;
		}
	}
	
	// HEADER / PREPROCESSOR
	
	private static void writeOpenHeader(StringBuffer header){
		header.append(intro + crlf);
		header.append("#ifndef " + headerName + crlf);
		header.append("#define " + headerName + crlf + crlf);
	}
	
	private static void writeCloseHeader(StringBuffer header){
		header.append("#endif // " + headerName + crlf);
	}
	
	private static void writeIncludes(StringBuffer header){
		header.append("#include <assert.h>" + crlf + crlf);
	}
	
	// FUNCTION DECLARATION
	
	private static void writeSignatures(StringBuffer header, IDfm dfm){
		header.append(getViolateSignature() + ";" + crlf + crlf);
		header.append(getSlotsFullSignature() + ";" + crlf + crlf);
		// write fsm function signatures
		header.append(getMoveSignature() + ";" + crlf + crlf);
		// write event Signatures
		for(Event e : dfm.getEvents().values()){
			header.append(getEventSignature(e) + "; // call this for signaling the occurrence of event " + e.name + crlf);
		}
		header.append(crlf);
	}
	
	// MOVE FUNCTION
	
	private static String getMoveSignature(){
		return "int " + moveFctName + "(int s, int e)";
	}
	
	private static String getMoveCall(String s, int e){
		return moveFctName + "(" + s + ", " + e + ")";
	}
	
	private static String getErrorStatement(){
		return "assert(\"" + errorMessage + "\" && 0);";
	}
	
	private static void writeMoveDefinition(StringBuffer header, IDfm dfm){
		StringBuffer indent = new StringBuffer();
		
		// open function body
		header.append(getMoveSignature() + "{" + crlf);
		addIndent(indent);
		
		// open state switch
		header.append(indent + "switch(s){" + crlf);
		
		// iterate cases
		for (DfmState s : dfm.getStates().values()){
			if (!dfm.getFinalStates().contains(s)){
				header.append(indent + "case " + s.getID() + " :" + crlf);
				addIndent(indent);
				
				// handle special cases
				if (s.getTransitions().isEmpty()){
					if (s.getDefaultTransition() == s){
						header.append(indent + "break;"+crlf);
					} else {
						if (dfm.getFinalStates().contains(s.getDefaultTransition())){
							header.append(indent + violateFctName + "();" + crlf);
						}
						header.append(indent + "return " + s.getDefaultTransition().getID() + ";" + crlf);
					}
				} else { // state has event transitions
					// open event switch
					header.append(indent + "switch(e){" + crlf);
					
					for (Event e : s.getTransitions().keySet()){
						// open event case
						header.append(indent + "case " + e.getID() + " :" + crlf);
						addIndent(indent);
						
						if (dfm.getFinalStates().contains(s.getTransitions().get(e))){
							header.append(indent + violateFctName + "();" + crlf);
						}
						header.append(indent + "return " + s.getTransitions().get(e).getID() + ";" + crlf);
						
						// close event case
						removeIndent(indent);
					}
					
					if (s.getDefaultTransition() != s){
						header.append(indent + "default :" + crlf);
						addIndent(indent);
						if (dfm.getFinalStates().contains(s.getDefaultTransition())){
							header.append(indent + violateFctName + "();" + crlf);
						}
						header.append(indent + "return + " + s.getDefaultTransition().getID() + ";" + crlf);
						removeIndent(indent);
					}
					
					// close event switch
					header.append(indent + "}" + crlf);
					header.append(indent + "break;" + crlf);
				}
				removeIndent(indent);	
			}
		}
		
		// close state switch
		header.append(indent + "}" + crlf);
		// write return
		header.append(indent + "return s;" + crlf);
		// close function body
		removeIndent(indent);
		header.append("}" + crlf);
		header.append(indent + crlf);
	}
	
	// ERROR FUNCTIONS
	
	private static void writeErrorFunctionDefinitions(StringBuffer header){
		
		writeViolateDefinition(header);
		
		writeSlotsFullDefinition(header);
		
	}
	
	private static String getViolateSignature(){
		return "void " + violateFctName + "()";
	}
	
	private static void writeViolateDefinition(StringBuffer header){
		StringBuffer indent = new StringBuffer();
		
		// open function body
		header.append(getViolateSignature() + "{" + crlf);
		addIndent(indent);
		
		// write violation statement
		header.append(indent + violateLabel + ": " + getErrorStatement() + crlf);
		
		// close function body
		removeIndent(indent);
		header.append("}" + crlf);
		header.append(indent + crlf);
	}
	
	private static String getSlotsFullStatement(){
		return "assert(\"The number of monitor slots is insufficient.\" && 0);";
	}
	
	private static String getSlotsFullSignature(){
		return "void " + slotsFullFctName + "()";
	}
	
	private static void writeSlotsFullDefinition(StringBuffer header){
		StringBuffer indent = new StringBuffer();
		
		// open function body
		header.append(getSlotsFullSignature() + "{" + crlf);
		addIndent(indent);
		
		// write slots full statement
		header.append(indent + slotsFullLabel + ": " + getSlotsFullStatement() + crlf);
		
		// close function body
		removeIndent(indent);
		header.append("}" + crlf);
		header.append(indent + crlf);
	}
	
	// EVENTS
	
	private static String getEventSignature(Event e){
		return "void " + eventToFunctionName(e) + "(" + parameterCollectionAsList(e.parameters) + ")";
	}
	
	private static String eventToFunctionName(Event e){
		return eventPrefix + e.name;
	}
	
	private static void writeEventDefinitions(StringBuffer header, IDfm dfm){
		StringBuffer indent = new StringBuffer();
		for (Event e : dfm.getEvents().values()){
			header.append(getEventSignature(e) + "{" + crlf);
			addIndent(indent);
			
			header.append(indent + "int _moved = 0;" + crlf);
			header.append(indent + crlf);
			header.append(indent + "// move matching monitors if present" + crlf);
			
			for (int i = 0; i < dfm.getMaximumNumberOfMonitors(); i++){
				header.append(indent + "if (" + dfm.getInitialState().getID() + " != " + getMonitorStateName(i));
				if (!e.parameters.isEmpty()){
					addIndent(indent); addIndent(indent);
					Iterator<Parameter> it = e.parameters.iterator();
					while (it.hasNext()){
						Parameter p = it.next();
						header.append(" &&" + crlf + indent + p.name + " == " + getStateVariableName(i, p.name));
					}
					
					removeIndent(indent); removeIndent(indent);
				}
				header.append("){" + crlf);
				addIndent(indent);
				
				header.append(indent + getMonitorStateName(i) + " = " + getMoveCall(getMonitorStateName(i), e.getID()) + ";" + crlf);
				header.append(indent + "_moved++;" + crlf);
				
				removeIndent(indent);
				header.append(indent + "}" + crlf);
			}
			
			header.append(indent + crlf);
			
			if (e.parameters.containsAll(dfm.getParameters().values())){
				
				header.append(indent + "if (0 == _moved){" + crlf);
				// open free monitor search
				addIndent(indent);
				header.append(indent + "// create new monitor if possible" + crlf);
				
				for (int i = 0; i < dfm.getMaximumNumberOfMonitors(); i++){
					// open check for free monitor
					header.append(indent + "if (" + dfm.getInitialState().getID() + " == " + getMonitorStateName(i) + "){" + crlf);
					addIndent(indent);
					
					header.append(indent + "_moved++;" + crlf);
					
					Iterator<Parameter> it = e.parameters.iterator();
					while (it.hasNext()){
						Parameter p = it.next();
						header.append(indent + getStateVariableName(i, p.name) + " = " + p.name + ";" + crlf);
					}
					
					header.append(indent + getMonitorStateName(i) + " = " + getMoveCall(getMonitorStateName(i), e.getID()) + ";" + crlf);
					
					header.append(indent + "return;" + crlf);
					
					// close check for free monitor
					removeIndent(indent);
					header.append(indent + "}" + crlf);
				}
				
				// close monitor search
				removeIndent(indent);
				header.append(indent + "}" + crlf + crlf);				
			}
			
			header.append(indent + slotsFullFctName + "();" + crlf);
			
			removeIndent(indent);
			header.append("}" + crlf + crlf);
		}
	}
	
	// STATES
	
	private static String getMonitorStateName(int monitor){
		return monitorVarPrefix + monitor;
	}
	
	private static String getStateVariableName(int monitor, String varName){
		return getMonitorStateName(monitor) + "_" + varName;
	}
	
	private static void writeMonitorState(StringBuffer header, IDfm dfm){

		for (int i = 0; i < dfm.getMaximumNumberOfMonitors(); i++){
			header.append("// monitor " + i + " state:" + crlf);
			header.append("int " + getMonitorStateName(i) + " = " + dfm.getInitialState().getID() + ";" + crlf);
			if (!dfm.getParameters().isEmpty()){
				for (Parameter p : dfm.getParameters().values()){
					header.append(p.type + " " + getStateVariableName(i, p.name) + ";" + crlf);
				}
			}
			header.append(crlf);
		}
	}
	
	// AUXILIARY
	
	private static String parameterCollectionAsList(Collection<Parameter> parameters){
		StringBuffer sb = new StringBuffer();
		Iterator<Parameter> it = parameters.iterator();
		while (it.hasNext()){
			sb.append(it.next());
			if (it.hasNext())
				sb.append(", ");
		}
		return sb.toString();
	}
	
	private static void addIndent(StringBuffer sb){
		sb.append(indentStr);
	}
	
	private static void removeIndent(StringBuffer sb){
		if (sb.length() > 0)
			sb.delete(sb.length()-indentStr.length(), sb.length());
	}
	
}
